g, h:GrpSig, f:MonHom(g,h), b:, p:|g|. (when b. (f(p))) = f(when b. p)  |h| 

latex

Up	groups 1
Definitions of Statement	MonHom(M1,M2), when b. p
Definitions	, ff, tt, P  Q, t  T, if b then t else f fi , when b. p, x:A. B(x), P & Q, P  Q, P  Q, Unit, , MonHom(M1,M2),
Lemmas	grp sig wf, monoid hom wf, grp car wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, monoid hom id, grp id wf